The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

getNodeFromEdge(S(S(x')), E(x, y)) → y
via(u, v, Cons(E(x, y), xs), edges) → via[Ite](!EQ(u, x), u, v, Cons(E(x, y), xs), edges)
getNodeFromEdge(S(0), E(x, y)) → x
member(x', Cons(x, xs)) → member[Ite](eqEdge(x', x), x', Cons(x, xs))
getNodeFromEdge(0, E(x, y)) → x
eqEdge(E(e11, e12), E(e21, e22)) → eqEdge[Ite](and(!EQ(e11, e21), !EQ(e12, e22)), e21, e22, e11, e12)
via(u, v, Nil, edges) → Nil
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
member(x, Nil) → False
reach(u, v, edges) → reach[Ite](member(E(u, v), edges), u, v, edges)
goal(u, v, edges) → reach(u, v, edges)

The (relative) TRS S consists of the following rules:

!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
via[Ite](True, u, v, Cons(E(x, y), xs), edges) → via[Let](u, v, Cons(E(x, y), xs), edges, reach(y, v, edges))
via[Let](u, v, Cons(x, xs), edges, Nil) → via(u, v, xs, edges)
via[Let](u, v, Cons(x, xs), edges, Cons(x', xs')) → Cons(x, Cons(x', xs'))
via[Ite](False, u, v, Cons(x, xs), edges) → via(u, v, xs, edges)
member[Ite](False, x', Cons(x, xs)) → member(x', xs)
reach[Ite](False, u, v, edges) → via(u, v, edges, edges)
reach[Ite](True, u, v, edges) → Cons(E(u, v), Nil)
member[Ite](True, x, xs) → True
eqEdge[Ite](False, e21, e22, e11, e12) → False
eqEdge[Ite](True, e21, e22, e11, e12) → True

Rewrite Strategy: INNERMOST

(1) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
eqEdge[Ite]/1
eqEdge[Ite]/2
eqEdge[Ite]/3
eqEdge[Ite]/4

(2) Obligation:

Runtime Complexity Relative TRS:
The TRS R consists of the following rules:

getNodeFromEdge(S(S(x')), E(x, y)) → y
via(u, v, Cons(E(x, y), xs), edges) → via[Ite](!EQ(u, x), u, v, Cons(E(x, y), xs), edges)
getNodeFromEdge(S(0), E(x, y)) → x
member(x', Cons(x, xs)) → member[Ite](eqEdge(x', x), x', Cons(x, xs))
getNodeFromEdge(0, E(x, y)) → x
eqEdge(E(e11, e12), E(e21, e22)) → eqEdge[Ite](and(!EQ(e11, e21), !EQ(e12, e22)))
via(u, v, Nil, edges) → Nil
notEmpty(Cons(x, xs)) → True
notEmpty(Nil) → False
member(x, Nil) → False
reach(u, v, edges) → reach[Ite](member(E(u, v), edges), u, v, edges)
goal(u, v, edges) → reach(u, v, edges)

The (relative) TRS S consists of the following rules:

!EQ(S(x), S(y)) → !EQ(x, y)
!EQ(0, S(y)) → False
!EQ(S(x), 0) → False
!EQ(0, 0) → True
and(False, False) → False
and(True, False) → False
and(False, True) → False
and(True, True) → True
via[Ite](True, u, v, Cons(E(x, y), xs), edges) → via[Let](u, v, Cons(E(x, y), xs), edges, reach(y, v, edges))
via[Let](u, v, Cons(x, xs), edges, Nil) → via(u, v, xs, edges)
via[Let](u, v, Cons(x, xs), edges, Cons(x', xs')) → Cons(x, Cons(x', xs'))
via[Ite](False, u, v, Cons(x, xs), edges) → via(u, v, xs, edges)
member[Ite](False, x', Cons(x, xs)) → member(x', xs)
reach[Ite](False, u, v, edges) → via(u, v, edges, edges)
reach[Ite](True, u, v, edges) → Cons(E(u, v), Nil)
member[Ite](True, x, xs) → True
eqEdge[Ite](False) → False
eqEdge[Ite](True) → True

Rewrite Strategy: INNERMOST

(3) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
via(0, v, Cons(E(S(y35_3), y), xs), edges) →⁺ via(0, v, xs, edges)
gives rise to a decreasing loop by considering the right hand sides subterm at position [].
The pumping substitution is [xs / Cons(E(S(y35_3), y), xs)].
The result substitution is [ ].

(4) BOUNDS(n^1, INF)